Lambda the Ultimate

For those interested in the new VB9 language, there is an interview on DDJ with me and my partners in crime Paul Vick, Amanda Silver, together with our more pointy haired, but good, friends Alan Griver, Rob Copeland, Jay Roxe.

The reason I got sold on software transactions, as opposed to joins, is this paper.

Jacob Matthews and Robby Findler bring us An Operational Semantics for R5RS Scheme (also available in PostScript):

This paper presents an operational semantics for the core of Scheme. Our specification improves over the existing R5RS denotational specification in four ways:

1. It is more complete, since it contains eval, quote, and dynamic-wind.
2. It models multiple values in a way that does not require changes to unrelated parts of the language.
3. It provides a more faithful model of Scheme's undefined order of evaluation.
4. It is executable, because it is encoded as a program in PLT Redex, a domain-specific language for writing operational semantics.

The executable specification allows others to experiment with our specification and allows us to build a specification test suite, which improves our confidence that our system is a faithful model of Scheme. In addition to contributing a specification of Scheme, this paper presents several novel modeling techniques for Felleisen Hieb-style rewriting semantics that we discovered while developing our R5RS Scheme semantics. All are applicable to a wider range of problems than the specific uses we have for them, and the fact that they combine seamlessly in our full R5RS model shows that they scale to real languages.

This looks like excellent work, as we've come to expect from the PLT folk.

The PLT Redex tool was previously discussed on LtU. If you're interested in checking it out, this page provides links to "everything you need to run PLT Redex and executable versions of every reduction system in the paper".

To be presented at the 2005 Workshop on Scheme and Functional Programming, Tallinn, Estonia, 24 September, 2005.

Thanks to Jens Axel Søgaard for bringing this paper to my attention.

Over the last couple of months, both my existence and my judgments have been questioned several times on my favorite programming languages waterhole :-)

In the mean time, I was busily working with the SQL, XML, C# and the Visual Basic teams on language integrated query, or as it is now called project LINQ. In particular since early this year I am collaborating with Amanda Silver, Paul Vick, and Rob Copeland and Alan Griver on what has become my programming language of choice Visual Basic.

If you look closely at the new features introduced to C# and Visual Basic in the context of LINQ, you will recognize many familiar concepts that are regularly discussed on LTU ranging from monads, to meta-programming, lambda expressions, XML programming, to the relationship between static and dynamic typing.

The LINQ project consists of a base pattern of query operators (compare to the monad primitives) such as Select (map), SelectMany (concatMap), Where (filter), OrderBy (sort), and GroupBy (groupBy) on top of which Visual Basic and C# define query comprehensions (compare to monad comprehensions) that  facilitate querying objects, relational data and XML. The C# syntax for query comprehensions is similar to FLWOR expressions, while the Visual Basic syntax stays close to SQL including aggregation.

In addition to the language extensions and base operators, LINQ provides two supplementary domain-specific APIs namely DLinq (compare to HaskellDB) for SQL relational data access, and XLinq (compare to HaXml) for XML hierarchical data access. Besides query comprehensions, Visual Basic provides deep XML integration with XML literals and XML late binding on top of XLinq (compare to Haskell Server Pages, XMl, Comega).

Both Visual Basic and C# have added several additional language extensions in support of LINQ, including local type inference (the type of local variable declarations are inferred from their initializers), lambda expressions (with type inference), local functions, anonymous types, object initializers, extension methods (static methods that can be called using instance method syntax), and meta-programming via expression trees (compare to type-based quote and quasi-quote).

Visual Basic adds some further enhancements to leverage the fact that it allows static typing where possible and dynamic typing where necessary in the form of relaxed delegates, improved nullable support, dynamic identifiers (makes writing meta-circular interpreters a breeze) and last but not least dynamic interfaces, or as I like to refer to them strong duck typing (compare to simplified qualified types/type classes).

LINQ general website: http://msdn.microsoft.com/netframework/future/linq/
VB9 specific website: http://msdn.microsoft.com/vbasic/future

Unlike the previous approaches, the latest implementation is generic. Shift and control share all the same code, and differ in only one boolean flag. Therefore, it becomes possible to mix different control operators in the same program. Furthermore, the latest implementation is direct rather than emulation (in terms of an object-level shift), therefore, it has the best performance. The code is surprisingly simple, compared with the previous implementation of 'control' by Sitaram and Felleisen, and does not require equality on continuations. All four delimited control operations do indeed reduce to call/cc and one global mutable cell, and hence have a quite simple CPS transform. That has been known since the paper by Chung-chieh Shan (Scheme Workshop, 2004). The current code shows that result more directly.

Oleg's implementation provides all four Friedman-Felleisen delimited control operators: from -F- (similar to cupto) to +F- (aka control) to +F+ (aka shift). The R5RS Scheme code is parameterized by two boolean flags: is-shift and keep-delimiter-upon-effect. All four combinations of the two flags correspond to four delimited control operators.

André Pang, Don Stewart, Sean Seefried, and Manuel M. T. Chakravarty. Plugging Haskell In (pdf). Proceedings of the ACM SIGPLAN Workshop on Haskell, 2004, pp. 10-21.

Extension languages enable users to expand the functionality of an application without touching its source code. Commonly, these languages are dynamically typed languages, such as Lisp, Python, or domain-specific languages, which support runtime plugins via dynamic loading of components. We show that Haskell can be comfortably used as a statically typed extension language, and that it can support type-safe dynamic loading of plugins using dynamic types.

Two of the authors also have a more recent paper (pdf) describing applications they've built using hs-plugins.

twill is a reimplementation of PBP, the "Python Browser Poseur"... The primary use for twill (as with PBP) is to do automated testing of Web applications via a straightforward declarative language. In addition to basic Web crawling, I wanted to be able to extend the language via Python, and I also wanted to be able to record things with maxq. Hence, twill.

B. Jacobs, Distributive laws for the Coinductive Solution of Recursive Equations, Information and Computation, to appear.

This paper illustrates the relevance of distributive laws for the solution of recursive equations, and shows that one approach for obtaining coinductive solutions of equations via infinite terms is in fact a special case of a more general approach using an extended form of coinduction via distributive laws...

Turi and Plotkin first investigated such a situation where one functor G describes the syntax of a programming language and the other functor F the behaviour of programs (terms) in that language. Having a distributive law GF => FG means that the behaviour on terms is well-defined, and leads to results like: (coalgebraic) bisimilarity is an (algebraic) congruence. Hence distributive laws capture where "algebra meets coalgebra".

Interesting stuff.

Be warned: This paper is highly technical, and requires familiarity with the fundamental notions of category theory.

Have you ever pressed the "stop" button in your web browser? Did it always work? Should PLs make it easier for developers to make it work?

Asynchronous Exceptions in Haskell

Asynchronous exceptions, such as timeouts, are important for robust, modular programs, but are extremely difficult to program with — so much so that most programming languages either heavily restrict them or ban them altogether. We extend our earlier work, in which we added synchronous exceptions to Haskell, to support asynchronous exceptions too. Our design introduces scoped combinators for blocking and unblocking asynchronous interrupts, along with a somewhat surprising semantics for operations that can suspend. Uniquely, we also give a formal semantics for our system.

PS: this was mentioned some time ago on LtU, but seems to be gone.

B. Jacobs, A Bialgebraic Review of Regular Expressions, Deterministic Automata and Languages, Technical Report ICIS-R05003, Institute for Computing and Information Sciences, Radboud University of Nijmegen.

This papers reviews the classical theory of deterministic automata and regular languages from a categorical perspective. The basis is formed by Rutten's description of the Brzozowski automaton structure in a coalgebraic framework. We enlarge the framework to a so-called bialgebraic one, by including algebras together with suitable distributive laws connecting the algebraic and coalgebraic structure of regular expressions and languages. This culminates in a reformulated proof via finality of Kozen's completeness result. It yields a complete axiomatisation of observational equivalence (bisimilarity) on regular expressions. We suggest that this situation is paradigmatic for (theoretical) computer science as the study of "generated behaviour".

Bart Jacobs. Bialgebras. Enough said.

Hans-J. Boehm. Threads Cannot Be Implemented As a Library. Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, June 2005, pp. 261-268. Official version. Technical report version.

In many environments, multi-threaded code is written in a language that was originally designed without thread support (e.g. C), to which a library of threading primitives was subsequently added. There appears to be a general understanding that this is not the right approach. We provide specific arguments that a pure library approach, in which the compiler is designed independently of threading issues, cannot guarantee correctness of the resulting code. We first review why the approach almost works, and then examine some of the surprising behavior it may entail. We further illustrate that there are very simple cases in which a pure library-based approach seems incapable of expressing an efficient parallel algorithm. Our discussion takes place in the context of C with Pthreads, since it is commonly used, reasonably well specified, and does not attempt to ensure type-safety, which would entail even stronger constraints. The issues we raise are not specific to that context.

The paper includes several interesting examples, and reminds us yet again of the importance of formally well defined semantics.